\begin{tabbing}
$\forall$\=$E$:Type, ${\it eq}$:EqDecider($E$), $T$:(Id$\rightarrow$Id$\rightarrow$Type), $V$:(Knd$\rightarrow$Id$\rightarrow$Type),\+
\\[0ex]${\it info}$:($E$$\rightarrow$(Id$\times$Id+(IdLnk$\times$$E$)$\times$Id)), ${\it pred?}$:($E$$\rightarrow$($E$+Unit)), ${\it val}$:($e$:$E$$\rightarrow$$V$(kind($e$),loc($e$))), ${\it when}$,
\\[0ex]${\it after}$:($x$:Id$\rightarrow$$e$:$E$$\rightarrow$$T$(loc($e$),$x$)), $p$:SESAxioms\{i:l\}($E$; $T$; ${\it pred?}$; ${\it info}$; ${\it when}$; ${\it after}$).
\-\\[0ex]ESAxioms(\=$E$;$T$;$\lambda$$l$,${\it tg}$. $V$(rcv($l$,${\it tg}$),destination($l$));\+
\\[0ex]$\lambda$$e$.loc($e$);$\lambda$$e$.kind($e$);${\it val}$;
\\[0ex]${\it when}$;${\it after}$;
\\[0ex]$\lambda$$l$,$e$. sends(${\it eq}$;IdLnkDeq;${\it pred?}$;${\it info}$;${\it val}$;1of($p$);$e$;$l$);$\lambda$$e$.sender($e$);$\lambda$$e$.
\\[0ex]index(${\it eq}$;IdLnkDeq;${\it pred?}$;${\it info}$;1of($p$);$e$);
\\[0ex]$\lambda$$e$.first($e$);$\lambda$$e$.pred($e$);
\\[0ex]$\lambda$$e$,${\it e'}$. $e$ $<$ ${\it e'}$)
\-
\end{tabbing}